Search for: All records

The hardware intellectual property (IP) cores from untrusted vendors are widely used, which has raised security concerns for system designers. Although formal methods provide powerful solutions for detecting malicious behaviors in hardware, the participation of manual work prevents the methods from practical applications. Information Flow Tracking (IFT) is a powerful approach to prevent sensitive information leakage. However, existing IFT solutions are either introducing overhead in hardware or lacking practical automatic working procedures. To alleviate these challenges, we propose a framework that fully automates information leakage detection in the gate level of hardware. This framework introduces Z3, an SMT solver, in checking the violation of the confidentiality automatically. On the other hand, a parser converting the gate-level hardware to the formal model is developed to further remove the manual workload. To validate the effectiveness, the proposed solution is tested on 11 gate-level netlist benchmarks. The Trojans leaking information from circuit outputs can be automatically detected. We also account for time consumption during the whole working procedure to show the efficiency of the proposed approach. 

Abstract For over 10 years, ModelSEED has been a primary resource for the construction of draft genome-scale metabolic models based on annotated microbial or plant genomes. Now being released, the biochemistry database serves as the foundation of biochemical data underlying ModelSEED and KBase. The biochemistry database embodies several properties that, taken together, distinguish it from other published biochemistry resources by: (i) including compartmentalization, transport reactions, charged molecules and proton balancing on reactions; (ii) being extensible by the user community, with all data stored in GitHub; and (iii) design as a biochemical ‘Rosetta Stone’ to facilitate comparison and integration of annotations from many different tools and databases. The database was constructed by combining chemical data from many resources, applying standard transformations, identifying redundancies and computing thermodynamic properties. The ModelSEED biochemistry is continually tested using flux balance analysis to ensure the biochemical network is modeling-ready and capable of simulating diverse phenotypes. Ontologies can be designed to aid in comparing and reconciling metabolic reconstructions that differ in how they represent various metabolic pathways. ModelSEED now includes 33,978 compounds and 36,645 reactions, available as a set of extensible files on GitHub, and available to search at https://modelseed.org/biochem and KBase.